The present invention relates generally to computational aspects of the design and testing of integrated circuits and other complex devices and systems, and more particularly to techniques for implementing so-called satisfiability algorithms involving such devices and systems.
Satisfiability (SAT) is a computationally-difficult problem which is central to many computer-aided design (CAD) and test applications. The SAT problem may be characterized as follows: given a boolean function F(x1, x2, . . . xn), find an assignment of binary values to the variables x1, x2, . . . xn, such that F is set to 1, or prove that no such assignment exists. Typically, F is expressed as a product-of-sums, which is also called conjunctive normal form (CNF). An example of a formula F in CNF is as follows:
F=(A+{overscore (B)}){circumflex over ( )}({overscore (A)}+B){circumflex over ( )}(A+{overscore (B)}).
In this example, the formula F includes two variables (A and B) and three clauses, each with two literals. The literals in the third clause are A+{overscore (B)}, where {overscore (B )} is an inverting literal and A is a non-inverting literal. The assignment (A=1, B=1) is a so-called xe2x80x9csatisfying assignment,xe2x80x9d i.e., it sets all the clauses and F to 1. Hence, the formula F given above is satisfiable. An example of an unsatisfiable formula Fxe2x80x2 is given by:
Fxe2x80x2=F{circumflex over ( )}({overscore (A)}+{overscore (B)})
In applications involving combinational circuits, the above-noted variables xj may represent primary inputs (PIs) of a given circuit, while F represents the primary output (PO) of that circuit. CAD and test applications that can be characterized as a SAT problem include, for example, timing verification, routing and routability analysis, fault diagnosis, logic synthesis and logic verification. SAT is also related to automatic test pattern generation (ATPG) algorithms, as it can be viewed as the problem of generating a test for a stuck-at-0 fault on a PO. An important component in ATPG is the so-called line justification problem, which deals with setting an internal signal to a given value, and corresponds to SAT on a subcircuit. Many other computationally-difficult problems, such as graph coloring, scheduling, theorem proving and constraint satisfaction problems, have also been mapped to SAT problems.
A significant drawback often associated with SAT problems is the amount of computation time required for their solution. Even with the most advanced SAT algorithms, difficult problems, such as those involving complex very-large-scale integration (VLSI) circuits, can require many hours of computation using powerful computers. A number of recently-developed techniques have attempted to simplify the SAT computation process through the use of reconfigurable hardware. Reconfigurable hardware is used in adaptive computing and other applications to implement logic circuit functions. A given set of reconfigurable hardware, which may be based on field programmable gate arrays (FPGAs) or other similar programmable logic devices, can be reconfigured so as to provide different logic functions at different times, thereby in effect providing the functionality of a complex circuit which would otherwise require substantially more hardware. Reconfigurable hardware platforms designed to facilitate SAT computation are referred to as xe2x80x9csatisfiers.xe2x80x9d
Another drawback associated with solving SAT problems using the above-noted reconfigurable hardware is the capacity and the cost of the reconfigurable hardware platform. Existing satisfiers are generally limited in the size of the problems they can handle by their available hardware capacity. As a result, any problem that does not fit within the available capacity of a given satisfier is automatically classified as xe2x80x9cout-of-boundsxe2x80x9d for that satisfier. Although conventional logic emulators can have a large capacity (up to several million gates), they are generally quite expensive (about $0.50 per emulated gate) and hence not easily affordable. However, most other hardware platforms that are reasonably priced do not provide sufficient capacity. A need therefore exists for improved techniques for solving satisfiability problems on reconfigurable hardware.
The invention provides a virtual logic system for solving satisfiability problems on reconfigurable hardware, which allows the reconfigurable hardware to solve problems much larger than its available capacity. In an illustrative embodiment, a set of reconfigurable hardware including a number of field programmable gate arrays (FPGAs) is configured to solve a satisfiability problem. The satisfiability problem is decomposed into a number of independent and disjoint subproblems, e.g., using a simple decomposition in conjunction with disjoint partitioning, such that each of the subproblems is implementable within a given one of the FPGAs without the need for any inter-FPGA communication. Each FPGA then independently determines a satisfiability indication for one of the subproblems. At least a subset of the FPGAs may each be used to process more than one of the subproblems.
In accordance with one aspect of the invention, a simple decomposition technique is provided for decomposing the satisfiability problem into a number of independent subproblems such that each of the subproblems is solvable by a single hardware element, e.g., a single FPGA, of a reconfigurable hardware platform. In one possible implementation, the simple decomposition technique utilizes a formula splitting process that is repeated recursively for k variables. If this decomposition process is represented by a binary OR tree with k levels, the subproblems to be solved are obtained at the terminal nodes of the tree. The OR relation between the two branches of a node means that solving one of the two subproblems is sufficient to solve the original problem. The more variables assigned, the smaller the subproblems become, although k should be limited since the number of subproblems is 2k. The resulting subproblems share all the variables that are not assigned, so the subproblems are not disjoint. Nevertheless, the subproblems are independent since the values of the shared variables do not have to be correlated, as different subproblems may obtain different satisfying vectors for the original problem.
In accordance with another aspect of the invention, a disjoint partitioning decomposition technique is provided which utilizes the above-noted simple decomposition technique in conjunction with disjoint partitioning to decompose a satisfiability problem into a number of independent and disjoint subproblems. One possible implementation of this disjoint partitioning decomposition utilizes a clause bipartitioning algorithm, which starts by creating a one-component cluster from each clause of a satisfiability formula in conjunctive normal form (CNF), and then repeatedly merges clusters based on a measure reflecting the number of common variables, until two final clause clusters are obtained such that their number of common variables is minimized. To separate these two clusters, at least some of their common variables are assigned. The algorithm tries tentative formula simplifications for both 0 and 1 assignments to each common variable, and evaluates the simplifications based on the reduction obtained in the set of common variables. If there are no common variables, the process continues recursively with the two disjoint sub formulas, both of which need to be satisfied. The recursion terminates when the current sub formulas fit into a target reconfigurable hardware platform. The disjoint partitioning decomposition technique generally results in a significantly smaller number of subproblems than the previously-described simple decomposition technique.
The decomposition techniques of the invention can effectively divide a satisfiability formula into independent subproblems that can be concurrently run by, e.g., multiple FPGAs, without the need for inter-FPGA signals or conventional multi-FPGA partitioning. In addition, the decomposition techniques of the invention are independent of the reconfigurable hardware platform, so they may be used with any satisfier.
Advantageously, the invention allows a reconfigurable hardware platform to process circuits much larger than the available capacity of the platform at the cost of a limited amount of additional processing time. For example, the invention allows any satisfier implemented with reconfigurable hardware, e.g., multiple FPGAs, to process circuits much larger than the available capacity of the FPGAs. Since the invention does not require any inter-FPGA signal routing, it can be implemented using a platform that is much simpler and cheaper than a conventional logic emulator. An additional benefit provided by the invention is a significant speed-up in computation time, e.g., up to three orders of magnitude, obtained by the concurrent solving of subproblems. Moreover, by avoiding the delays associated with inter-FPGA signal routing, a virtual logic system in accordance with the invention can operate at a substantially higher clock frequency than would otherwise be possible. Another advantage is that the virtual logic system of the invention is easily scalable to accommodate satisfiability problems of any size, e.g., larger problems can be handled simply by using additional or larger FPGAs.